﻿using System;
using System.Diagnostics.Contracts;
using System.IO;

namespace O1.Kernel.IO
{
    [ContractVerification(true)]
    internal abstract class InputAdapter
    {
        private const int Size16K = 1024 * 16;

        [ThreadStatic]
        private static byte[] rawBuffer;

        private int max;

        protected InputAdapter()
        {
            Contract.Ensures(rawBuffer != null);
            Contract.Ensures(rawBuffer.Length == Size16K);

            if (rawBuffer == null)
            {
                rawBuffer = new byte[Size16K];
            }

            Contract.Assume(rawBuffer.Length == Size16K);
        }

        public int CurrentOffset { get; private set; }

        public bool EndOfBuffer
        {
            get
            {
                return this.max < 0;
            }
        }

        public byte[] Buffer
        {
            get
            {
                return rawBuffer;
            }
        }

        internal bool MoveNext(int nextSize, out int lastOffset)
        {
            Contract.Requires(0 <= nextSize);
            Contract.Requires(Size16K > nextSize);
            Contract.Ensures(rawBuffer.Length == Size16K);
            Contract.Ensures(-1 <= Contract.ValueAtReturn<int>(out lastOffset));
            Contract.Ensures(
                Contract.Result<bool>() == false ||
                (Contract.Result<bool>() == true && Contract.ValueAtReturn<int>(out lastOffset) + nextSize < this.Buffer.Length));

            if (this.max == -1)
            {
                lastOffset = -1;
                return false;
            }

            var nextOffset = this.CurrentOffset + nextSize;
            if (nextOffset >= this.max)
            {
                Contract.Assume(this.max >= this.CurrentOffset);

                var bytesRead = this.ShiftBuffer(nextSize);
                
                // This condition means no additional bytes were available, but the 
                // next read expects additional bytes. Should this throw?
                if (bytesRead == 0)
                {
                    this.max = -1;
                    lastOffset = this.CurrentOffset;

                    // The caller can opt to read the remainder by testing for -1 last offset,
                    // or decide this is a failure scenario with invalid data.
                    return false;
                }

                Contract.Assume(bytesRead < rawBuffer.Length);
                Contract.Assume(bytesRead >= nextSize);

                this.max = bytesRead;
                this.CurrentOffset = nextSize;
                lastOffset = 0;
                return true;
            }

            lastOffset = this.CurrentOffset;
            this.CurrentOffset = nextOffset;
            return true;
        }

        protected abstract int ReadToBuffer(byte[] buffer, int offset, int count);

        private int ShiftBuffer(int nextSize)
        {
            Contract.Requires(this.max >= this.CurrentOffset);

            var buffer = rawBuffer;
            var remainder = this.max - this.CurrentOffset;
            if (remainder + nextSize >= Size16K)
            {
                throw new InvalidOperationException(ExceptionText.SizeExceeds8KBuffer.ToFormat(nextSize));
            }

            Contract.Assert(this.max - this.CurrentOffset + nextSize < this.Buffer.Length);
            Contract.Assert(remainder > -1);
            Contract.Assert(this.max < buffer.Length);
            Contract.Assert(this.CurrentOffset + remainder < buffer.Length);

            if (remainder > 0)
            {
                Array.Copy(buffer, this.CurrentOffset, buffer, 0, remainder);
            }

            var bytesRead = this.ReadToBuffer(buffer, remainder, Size16K - remainder) + remainder;
            Contract.Assume(this.max - this.CurrentOffset + nextSize < this.Buffer.Length);
            return bytesRead;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(rawBuffer.Length == Size16K);
            Contract.Invariant(this.max < Size16K);
            Contract.Invariant(this.max == -1 || this.max >= this.CurrentOffset);
            Contract.Invariant(0 <= this.CurrentOffset);
        }
    }
}
